FDL - Step of Proof: ite_rw

Step of Proof: ite_rw_false

9,38

Inference at *
Iof proof for Lemma ite rw false:

T:Type, b:

, x,y:T. (

(

b))

(if b then x else y fi = y)

by InteriorProof ((((RepD)

CollapseTHENM (SplitOnConclITE))

)

CollapseTHEN (

CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t

CollapseTHEN () inil_term)))

Definitions , t T, x:A. B(x), False, P Q, A

Lemmas not wf, bnot wf, assert wf, bool wf

Definitions	, t T, x:A. B(x), False, P Q, A
Lemmas	not wf, bnot wf, assert wf, bool wf